Inference at * 1 1 2 1 
Iof proof for Lemma decidable implies better:

.....assertion..... NILNIL

1. P : 
2. Q : x:P.
3. P
4. P  Dec(Q)
  (P  Q)   

latex

 by MemCD THEN Auto 

latex

 .

Definitions

, t  T, A, P  Q, False